Issue1886-relevance.agda:7,9-10
Unexpected modality/relevance annotation in .A
when checking the definition of D
